/*
 * Copyright 2011, 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree;

import java.io.File;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.Queue;
import java.util.Stack;

import javax.xml.parsers.DocumentBuilderFactory;
import javax.xml.parsers.FactoryConfigurationError;
import javax.xml.parsers.ParserConfigurationException;
import javax.xml.transform.OutputKeys;
import javax.xml.transform.Transformer;
import javax.xml.transform.TransformerConfigurationException;
import javax.xml.transform.TransformerException;
import javax.xml.transform.TransformerFactory;
import javax.xml.transform.TransformerFactoryConfigurationError;
import javax.xml.transform.dom.DOMSource;
import javax.xml.transform.stream.StreamResult;

import org.w3c.dom.Document;
import org.w3c.dom.Element;

import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePatternFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.CoefficientChooser;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.SolverInformation;
import de.wenzelmf.booleanFunction.lpb.util.LPBCombinatorialConstants;
import de.wenzelmf.booleanFunction.util.IntegerValue;
import de.wenzelmf.booleanFunction.util.Tuple;

/**
 * This class provides methods to create a splitting tree given a DNF, i.e. it creates all
 * recursive solutions required for the combinatorial algorithm.
 * 
 * To create the complete tree you must call one of the {@code createTree} methods first.
 * 
 * There's also a method that creates the tree in a synchronized way.
 * 
 * @see #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)
 * @see #createTreeSynchronized(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class SplittingTree
{
	/*
	 * The root node of the tree.
	 */
	private SplittingTreeNode root;
	
	/*
	 * The The variable setting that gives us some global information about
	 * the variables.
	 */
	private VariableSetting variables;
	
	/**
	 * Construct a new splitting tree given a start node.
	 * 
	 * @param root The root node of the tree.
	 */
	public SplittingTree(StartNode root, OccurrencePatternFactory opFactory)
	{
		this.root = root;
		this.variables = root.getSetting(opFactory);
	}
	
	/**
	 * Private constructor that creates a new splitting tree given a context.
	 * 
	 * @param dnf The DNF of the root node.
	 * @param context The The variable setting that gives us some global information about
	 * the variables.
	 */
	private SplittingTree(DNF dnf, OccurrencePatternFactory opFactory, TreeContext context)
	{
		this(new StartNode(dnf, context), opFactory);
	}
	
	/**
	 * Construct a new splitting tree given the DNF of the root node and the columns of the resulting
	 * table (the {@code columns} value is only used for efficiency reasons).
	 * 
	 * @param dnf The DNF of the root node.
	 * @param columns The columns of the resulting table (for efficiency reasons).
	 */
	public SplittingTree(DNF dnf, int columns, OccurrencePatternFactory opFactory)
	{
		this(new StartNode(dnf, new TreeContext(columns)), opFactory);
	}
	
	/**
	 * Construct a new splitting tree given the DNF of the root node.
	 * 
	 * The DNF of the root node.
	 * 
	 * @param dnf
	 */
	public SplittingTree(DNF dnf, OccurrencePatternFactory opFactory)
	{
		this(dnf, opFactory, new TreeContext());
	}
	
	/**
	 * Private constructor for internal use.
	 * 
	 * @param node The root node of the Tree.
	 * @param variables The variable setting of this tree.
	 */
	private SplittingTree(SplittingTreeNode node, VariableSetting variables)
	{
		this.root = node;
		this.variables = variables;
	}
	
	// TODO: do many, many tests!
	// especially: the two generated nodes may share the same DNF object
	// but this should be ok because we only use read operations?
	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 * @throws InterruptedException If another thread has interrupted the current thread, see
	 * <a href="http://docs.oracle.com/javase/1.5.0/docs/api/java/lang/Thread.html#join%28%29">Java Thread class.</a>.
	 */
	public void createTreeSynchronized(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory, boolean releaseMemory) throws NotSymmetricException, InterruptedException
	{
		if(root.isFinal())
		{
			createTree(symmetryTest, factory, clauseFactory, dnfFactory, releaseMemory);
			return;
		}
		root.split(symmetryTest, factory, variables, clauseFactory, dnfFactory);
		
		// create a tree for each of the successors and solve each of them in a thread
		SplittingTreeNode r1 = root.upperChild, r2 = root.lowerChild;
		// first create a copy of the variable setting
		// create for each of them a copy
		// TODO: maybe they can use the same? 
		String[] variables1 = new String[this.variables.size() - 1];
		String[] variables2 = new String[this.variables.size() - 1];
		
		// TODO: size?
		HashMap<String, Integer> pos1 = new HashMap<String, Integer>(this.variables.size() * 2);
		HashMap<String, Integer> pos2 = new HashMap<String, Integer>(this.variables.size() * 2);
		for(int i = 1; i < variables.size(); i++)
		{
			String v = variables.sortedVariables[i];
			variables1[i - 1] = v;
			variables2[i - 1] = v;
			pos1.put(v, i - 1);
			pos2.put(v, i - 1);
		}
		VariableSetting vs1 = new VariableSetting(variables1, pos1);
		VariableSetting vs2 = new VariableSetting(variables2, pos2);
		
		// little cheating
		
		r1.column = 0;
		r1.row = 0;
		
		r2.column = 0;
		r2.row = 0;
		
		r1.context = new TreeContext(variables1.length);
		r1.context.addNode(r1);
		
		r2.context = new TreeContext(variables1.length);
		r2.context.addNode(r2);
		
		r1.upperParent = null;
		r1.lowerParent = null;
		
		r2.upperParent = null;
		r2.lowerParent = null;
		
		
		final SplittingTree t1 = new SplittingTree(r1, vs1), t2 = new SplittingTree(r2, vs2);
		
		SplitThread threadOne = new SplitThread(t1, symmetryTest, factory, clauseFactory, dnfFactory, releaseMemory);
		SplitThread threadTwo = new SplitThread(t2, symmetryTest, factory, clauseFactory, dnfFactory, releaseMemory);
		
		threadOne.start();
		threadTwo.start();
		
		threadOne.join();
		threadTwo.join();
		
		if(threadOne.exception != null)
		{
			throw threadOne.exception;
		}
		
		if(threadTwo.exception != null)
		{
			throw threadTwo.exception;
		}
		
		// merge the two results
		// adjust all column, row and context values!
		// means: undo the cheating
		
		r1.column = 1;
		r1.row = 0;
		
		r2.column = 1;
		r2.row = 1;
		
		r1.lowerParent = root;
		r2.upperParent = root;

		boolean first = true;
		for(Iterator<SplittingTreeNode> col : t1.getContext())
		{
			// move all the nodes one to the right
			// i.e. increase column value by one
			// but not for the first column (we already did this before)
			if(first)
			{
				first = false;
			}
			else
			{
				while(col.hasNext())
				{
					SplittingTreeNode n = col.next();
					n.column++;
					root.context.addNode(n);
					n.context = root.context;
				}
			}
		}
		
		first = true;
		for(Iterator<SplittingTreeNode> col : t2.getContext())
		{
			// do the same as before, but this time also adjust the row value
			if(first)
			{
				first = false;
			}
			else
			{
				while(col.hasNext())
				{
					SplittingTreeNode n = col.next();
					n.column++;
					n.row = root.context.addNode(n);
					n.context = root.context;
				}
			}
		}
		
	}
	
	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean, OccurrencePatternFactory)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeSynchronized(boolean symmetryTest, OccurrencePatternFactory factory) throws NotSymmetricException, InterruptedException
	{
		this.createTreeSynchronized(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeSynchronized(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException, InterruptedException
	{
		this.createTreeSynchronized(symmetryTest, factory, clauseFactory, dnfFactory, true);
	}

	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean, OccurrencePatternFactory, boolean)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeSynchronized(boolean symmetryTest, OccurrencePatternFactory factory, boolean releaseMemory) throws NotSymmetricException, InterruptedException
	{
		this.createTreeSynchronized(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory, releaseMemory);
	}
	
	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean, boolean)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeSynchronized(boolean symmetryTest, boolean releaseMemory) throws NotSymmetricException, InterruptedException
	{
		this.createTreeSynchronized(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, releaseMemory);
	}
	
	/**
	 * Creates the splitting tree but uses two threads to solve two subproblems independently.
	 * 
	 * Creates the tree as the method {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and all variations of this method. But it first calls the {@link SplittingTreeNode#split(boolean,
	 * OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} on the root node of the
	 * tree. Then it creates two new SplittingTrees for both successor nodes. Each of the node
	 * is created in its own thread. Once both trees have been created the results get merged. 
	 * 
	 * For details see {@link #createTree(boolean)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeSynchronized(boolean symmetryTest) throws NotSymmetricException, InterruptedException
	{
		this.createTreeSynchronized(symmetryTest, LPBCombinatorialConstants.defaultOPFactory);
	}
	
	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * For details see {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory, boolean releaseMemory) throws NotSymmetricException
	{
		Stack<SplittingTreeNode> waiting = new Stack<SplittingTreeNode>();
		waiting.push(root);
		while(!waiting.isEmpty())
		{
			SplittingTreeNode head = waiting.pop();
			if(head.isFinal() || head.alreadySplit)
			{
				continue;
			}
			head.split(symmetryTest, factory, variables, clauseFactory, dnfFactory);
			if(releaseMemory)
			{
				head.destroyContent();
			}
			SplittingTreeNode child1, child2;
			child1 = head.upperChild;
			child2 = head.lowerChild;
			
			if(!child2.isAlreadySplit())
			{
				waiting.push(child2);
			}
			if(!child1.isAlreadySplit())
			{
				waiting.push(child1);
			}
		}
	}
	
	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants} and releases the
	 * memory in the nodes after calling the split method.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest, OccurrencePatternFactory factory) throws NotSymmetricException
	{
		this.createTreeDepthFirst(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and releases the memory after splitting the nodes.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException
	{
		this.createTreeDepthFirst(symmetryTest, factory, clauseFactory, dnfFactory, true);
	}

	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest, OccurrencePatternFactory factory, boolean releaseMemory) throws NotSymmetricException
	{
		this.createTreeDepthFirst(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory, releaseMemory);
	}
	
	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest, boolean releaseMemory) throws NotSymmetricException
	{
		this.createTreeDepthFirst(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, releaseMemory);
	}
	
	/**
	 * Creates the splitting tree but creates the tree in a depth first manner.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}
	 * and releases the memory after splitting the nodes.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTreeDepthFirst(boolean symmetryTest) throws NotSymmetricException
	{
		this.createTreeDepthFirst(symmetryTest, LPBCombinatorialConstants.defaultOPFactory);
	}
	
	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory, boolean releaseMemory) throws NotSymmetricException
	{
		//VariableSetting variables = root.getSetting(factory);
		//this.variables = variables;
		
		Queue<SplittingTreeNode> waiting = new LinkedList<SplittingTreeNode>();
		waiting.offer(root);
		while(!waiting.isEmpty())
		{
			SplittingTreeNode head = waiting.poll();
			if(head.isFinal() || head.alreadySplit)
			{
				continue;
			}
			head.split(symmetryTest, factory, variables, clauseFactory, dnfFactory);
			if(releaseMemory)
			{
				head.destroyContent();
			}
			SplittingTreeNode child1, child2;
			child1 = head.upperChild;
			child2 = head.lowerChild;
			
			if(!child1.isAlreadySplit())
			{
				waiting.offer(child1);
			}
			if(!child2.isAlreadySplit())
			{
				waiting.offer(child2);
			}
		}
	}
	
	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants} and releases the
	 * memory in the nodes after calling the split method.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest, OccurrencePatternFactory factory) throws NotSymmetricException
	{
		this.createTree(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * and releases the memory after splitting the nodes.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param clauseFactory The factory that is used to create the clauses.
	 * @param dnfFactory The factory that is used to create the DFNs.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest, OccurrencePatternFactory factory,
			ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException
	{
		this.createTree(symmetryTest, factory, clauseFactory, dnfFactory, true);
	}

	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest, OccurrencePatternFactory factory, boolean releaseMemory) throws NotSymmetricException
	{
		this.createTree(symmetryTest, factory, LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory, releaseMemory);
	}
	
	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * @param releaseMemory If this value is {@code true} the {@link SplittingTreeNode#destroyContent()} method
	 * is called after calling the {@code split} method on that node to release some memory, 
	 * this means that the DNF and occurrence patterns are not longer accessible.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest, boolean releaseMemory) throws NotSymmetricException
	{
		this.createTree(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, releaseMemory);
	}
	
	/**
	 * Try to create the complete tree.
	 * 
	 * It may throw a {@link NotSymmetricException} if during the execution a set of not symmetric
	 * variables is found.
	 * 
	 * It just calls {@link #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
	 * with the default factories as defined in {@link LPBCombinatorialConstants}
	 * and releases the memory after splitting the nodes.
	 * 
	 * @param symmetryTest If this parameter is {@code true} a symmetry test is performed (to check
	 * if this DNF can be represented by a single LPB), if you don't perform this test you may get
	 * an incorrect solution.
	 * 
	 * @throws NotSymmetricException If a set <i>X</i> of variables is found s.t. the variables in
	 * <i>X</i> are not symmetric in the corresponding DNF.
	 */
	public void createTree(boolean symmetryTest) throws NotSymmetricException
	{
		this.createTree(symmetryTest, LPBCombinatorialConstants.defaultOPFactory);
	}
	
	/**
	 * Creates a String representation of this tree.
	 * 
	 * @return A String representation.
	 */
	@Override
	public String toString()
	{
		StringBuilder result = new StringBuilder();
		
		int c = 0;
		
		for(Iterator<SplittingTreeNode> column : root.context)
		{
			result.append("############ Column ");
			result.append(c++);
			result.append(" ############\n");
			
			while(column.hasNext())
			{
				result.append(column.next());
				result.append("\n-------------\n");
			}
		}
		
		return result.toString();
	}
	
	/**
	 * Return the root node of this tree.
	 * 
	 * @return The root node of the tree.
	 */
	public SplittingTreeNode getRoot()
	{
		return root;
	}
	
	/**
	 * Return the tree context of the root node.
	 * 
	 * @return The tree context of the root node.
	 * 
	 * @see StartNode#getContext().
	 */
	public TreeContext getContext()
	{
		return root.context;
	}
	
	/**
	 * Calculate the minimum and maximum degree (first component minimum degree second component
	 * minimum degree) in the specified {@code column} in the table.
	 * 
	 * This method calculates all minimum and maximum degrees for nodes in column <i>k</i>
	 * (assigns the values to the corresponding nodes using the solver information
	 * {@link SolverInformation#setCoefficient(int, int)}).
	 * Returns the max and min values that are required to compute the coefficient a<sub>k</sub>
	 * (first component is max and second value is min).
	 * 
	 * If max + 1 = min we have a conflict to solve. Therefore the
	 * {@link SolverInformation#solveConflict(int, DNF, IntegerValue, IntegerValue, TreeContext, SplittingTree)}
	 * method is called to solve this conflict.
	 *
	 * @param column The column in which the minimum and maximum degrees should be calculated.
	 * @param coefficientChooser The CoefficientChooser object that is used to 
	 * @param information Solver information object that is used to get and to set the values of the
	 * minimum and maximum degrees and coefficients.
	 * 
	 * @return The tuple (max, min) that is required to calculate a<sub>k</sub>.
	 */
	public Tuple<IntegerValue, IntegerValue> handleColumn(int column,CoefficientChooser coefficientChooser,
			SolverInformation information)
	{
		SplittingTreeNode last = null;
		IntegerValue minSoFar = null;
		IntegerValue maxSoFar = null;
		int cols = root.context.size();
		int sum = 0;
		// TODO: maybe do it more neatly but it's hard if the coefficients can change...
		for(int i = column + 1; i < cols; i++)
		{
			sum += information.getCoefficient(i);
		}
		IntegerValue sVal = new IntegerValue(sum);
		Iterator<SplittingTreeNode> level = root.context.getColumn(column);
		while(level.hasNext())
		{
			SplittingTreeNode n = level.next();
			if(n.isFinal())
			{
				// its DNF is either true or false
				if(getDNFValue(n.getDnf()))
				{
					information.setInterval(n, 
							new Tuple<IntegerValue, IntegerValue>( IntegerValue.NEGATIVE_INFINITY,
							IntegerValue.ZERO ));
				}
				else
				{
					information.setInterval(n, new Tuple<IntegerValue, IntegerValue>(sVal,
							IntegerValue.POSITIVE_INFINITY));
				}
			}
			else
			{
				IntegerValue s0, s1, b0, b1, s, b;
				Tuple<IntegerValue, IntegerValue> upperInterval, lowerInterval;
				upperInterval = information.getInterval(n.upperChild);
				lowerInterval = information.getInterval(n.lowerChild);
				s0 = upperInterval.getFirst();
				s1 = lowerInterval.getFirst();
				b0 = upperInterval.getSecond();
				b1 = lowerInterval.getSecond();
				
				int coefficient = information.getCoefficient(column + 1);
				s = IntegerValue.max(s0, s1.add(coefficient));
				b = IntegerValue.min(b0, b1.add(coefficient));
				
				information.setInterval(n, new Tuple<IntegerValue, IntegerValue>(s, b));
			}
			// TODO: not sure but it should work?
			if(last != null && n.upperParent != null && n.upperParent.upperChild == last)
			{
				// update min and max values
				
				Tuple<IntegerValue, IntegerValue> lastInterval, currentInterval;
				lastInterval = information.getInterval(last);
				currentInterval = information.getInterval(n);
				
				IntegerValue dif1 = lastInterval.getFirst().subtract(currentInterval.getSecond());
				IntegerValue dif2 = lastInterval.getSecond().subtract(currentInterval.getFirst());
				
				if(minSoFar == null)
				{
					maxSoFar = dif1;
					minSoFar = dif2;
				}
				else
				{
					maxSoFar = IntegerValue.max(maxSoFar, dif1);
					minSoFar = IntegerValue.min(minSoFar, dif2);
				}
			}
			last = n;
		}
		// try to choose value between maxSoFar and minSoFar
		if(maxSoFar == null || minSoFar == null)
		{
			return new Tuple<IntegerValue, IntegerValue>(null, null);
		}
		if(maxSoFar.isNumber() && minSoFar.isNumber() && maxSoFar.intValue() + 1 == minSoFar.intValue())
		{
			// we have a conflict. so solve it...
			Tuple<IntegerValue, IntegerValue> newValues = information.solveConflict(column, root.dnf,
					maxSoFar, minSoFar, root.context, this);
			maxSoFar = newValues.getFirst();
			minSoFar = newValues.getSecond();
		}
		return new Tuple<IntegerValue, IntegerValue>(maxSoFar, minSoFar);
	}
	
	/**
	 * Returns the variable setting that gives some information about the variables in the DNF
	 * of the root node.
	 * 
	 * This method returns {@code null} as long as none of the {@code createTree} methods has been called.
	 * After calling one of the methods the initial setting is created from the root node of the DNF.
	 * 
	 * @return The variable setting that gives some information about the variables in the DNF
	 * of the root node, {@code null} before one of the {@code createTree} methods has been called..
	 * 
	 * @see #createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)
	 */
	public VariableSetting getVariables()
	{
		return variables;
	}
	
	/**
	 * Returns {@code true} if this DNF represents <i>true</i> and {@code false} otherwise.
	 * 
	 * This method should be only used if this node is a final node, i.e. it represents really
	 * <i>true</i> or <i>false</i>.
	 * 
	 * @param dnf The DNF to check.
	 */
	private boolean getDNFValue(DNF dnf)
	{
		return dnf.size() != 0;
	}
	// TODO: what about a synchronized version of create tree?
	// after creating the first node (this is a main node!)
	// we obtain two successors
	// maybe create just two trees with both successors and solve each of them in a thread
	// then bring solutions together
	
	/**
	 * Creates an XML Document from this SplittingTree - see documentation for XML file format.
	 * 
	 * @return A XML Document representing this tree.
	 * 
	 * @throws FactoryConfigurationError See <a href="http://docs.oracle.com/javase/1.5.0/docs/api/javax/xml/parsers/DocumentBuilderFactory.html#newInstance%28%29">here</a>.
	 * @throws ParserConfigurationException See <a href="http://docs.oracle.com/javase/1.5.0/docs/api/javax/xml/parsers/DocumentBuilderFactory.html#newDocumentBuilder%28%29">here</a>.
	 */
	// TODO: use XML exception here (from the parser package)
	// TODO: use static final fields for the string constants?
	public Document toXMLDocument() throws ParserConfigurationException, FactoryConfigurationError
	{
		
		DocumentBuilderFactory documentBuilderFactory = DocumentBuilderFactory.newInstance();
		
		TreeContext context = getContext();
		
		Document result = documentBuilderFactory.newDocumentBuilder().newDocument();
		
		Element root = result.createElement("splittingTree");
	
		// root.setAttribute("variables", variables.toString());
		root.setAttribute("columns", "" + context.size());
		
		result.appendChild(root);
		
		int col = 0;
		for(Iterator<SplittingTreeNode> column : context)
		{
			// create column entry for each column
			Element columnEntry = result.createElement("column");
			columnEntry.setAttribute("columnID", "" + col);
			columnEntry.setAttribute("nodes", "" + context.getColumnSize(col));
			
			while(column.hasNext())
			{
				SplittingTreeNode n = column.next();
				Element nodeEntry = n.getXMLElement(result);
				
				columnEntry.appendChild(nodeEntry);
			}
			col++;
			root.appendChild(columnEntry);
		}
		result.setXmlStandalone(true);
		return result;
	}
	
	/**
	 * Writes the Splitting tree as an XML file - uses the {@link #toXMLDocument()} method to create the
	 * document and writes it to the specified file.
	 * 
	 * @param file The file to write the tree to.
	 * 
	 * @throws ParserConfigurationException See <a href="http://docs.oracle.com/javase/1.5.0/docs/api/javax/xml/parsers/DocumentBuilderFactory.html#newDocumentBuilder%28%29">here</a>.
	 * @throws FactoryConfigurationError See <a href="http://docs.oracle.com/javase/1.5.0/docs/api/javax/xml/parsers/DocumentBuilderFactory.html#newInstance%28%29">here</a>.
	 * @throws TransformerException See <a href="http://docs.oracle.com/javase/1.4.2/docs/api/javax/xml/transform/Transformer.html#transform%28javax.xml.transform.Source,%20javax.xml.transform.Result%29>here</a>.
	 * @throws TransformerFactoryConfigurationError See <a href="http://docs.oracle.com/javase/1.4.2/docs/api/javax/xml/transform/TransformerFactory.html#newInstance%28%29">here</a>.
	 * @throws TransformerConfigurationException See <a href="http://docs.oracle.com/javase/1.4.2/docs/api/javax/xml/transform/TransformerFactory.html#newTransformer%28%29">here</a>.
	 * 
	 * @see #toXMLDocument()
	 */
	// TODO: TransformerException link doesnt work
	public void writeXML(File file) throws ParserConfigurationException, FactoryConfigurationError, 
		TransformerException, TransformerFactoryConfigurationError, TransformerConfigurationException
	{
		TransformerFactory factory = TransformerFactory.newInstance();
		Transformer transformer = factory.newTransformer();
		transformer.setOutputProperty(OutputKeys.INDENT, "yes");
		transformer.setOutputProperty(OutputKeys.STANDALONE, "yes");
		transformer.setOutputProperty("{http://xml.apache.org/xslt}indent-amount", "3");
		DOMSource source = new DOMSource(toXMLDocument());
		StreamResult sr = new StreamResult(file);
		transformer.transform(source, sr);
	}
	
	/**
	 * Internal class that is used to create a splitting tree in a thread.
	 * 
	 * @author Fabian Wenzelmann
	 * @version 1.0
	 *
	 */
	private class SplitThread extends Thread
	{
		/**
		 * Reference to the splitting tree (the tree's {@link 
		 * createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
		 * will be called.
		 */
		// for all other fields see the documentation of createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}.
		SplittingTree t;
		boolean symmetryTest;
		OccurrencePatternFactory factory;
		ClauseFactory clauseFactory;
		DNFFactory dnfFactory;
		boolean releaseMemory;
		/**
		 * This value is set to a value {@code != null} if the exception is thrown when the run method
		 * is called.
		 */
		NotSymmetricException exception;
		
		/**
		 * Creates a new Thread (you have to start the thread by hand).
		 * 
		 * @param t The {@link SplittingTree} that will be created by calling the not synchronized
		 * method {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}
		 * @param symmetryTest see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 * @param factory see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 * @param clauseFactory see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 * @param dnfFactory see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 * @param releaseMemory see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 */
		public SplitThread(SplittingTree t, boolean symmetryTest, OccurrencePatternFactory factory,
				ClauseFactory clauseFactory, DNFFactory dnfFactory, boolean releaseMemory)
		{
			this.t = t;
			this.symmetryTest = symmetryTest;
			this.factory = factory;
			this.clauseFactory = clauseFactory;
			this.dnfFactory = dnfFactory;
			this.releaseMemory = releaseMemory;
			this.exception = null;
		}
		
		/**
		 * Tries to create the tree by calling the see {@link {@link createTree(boolean, OccurrencePatternFactory, ClauseFactory, DNFFactory, boolean)}}
		 * method.
		 * 
		 * If a {@link NotSymmetricException} is thrown the field {@code exception} of this thread is
		 * set to this exception. So if the {@code exception} value of the thread is {@code null}
		 * after the thread is finished no exception was thrown. Otherwise the thrown exception can be
		 * found in the {@code exception} field.
		 */
		@Override
		public void run()
		{
			try
			{
				t.createTree(symmetryTest, factory, clauseFactory, dnfFactory, releaseMemory);
			}
			catch(NotSymmetricException e)
			{
				exception = e;
			}
		}
	}
}